es:ES, T, A:Type, l:IdLnk, tg, a:Id, ds:x:Id fp Type, P:(State(ds)),
f:({s:State(ds)| (P(s))} AT).
weak-precond-send-p(es;T;A;l;tg;a;ds;P;f)
 discrete-weak-precond-send-p(es;T;A;l;tg;a;ds;P;f) 

latex

Definitions

t  T, {T}, P  Q, x:A. B(x), SQType(T), loc(e), s ~ t, P  Q, x:A  B(x), b, ES, Type, IdLnk, Atom$n, Id, a:A fp B(a), xdom(f). v=f(x)   P(x;v), @i discrete ds, x:AB(x), e@i. P(e), False, s = t, (e <loc e'), (e < e'), A, e loc e' , e c e', t.1, E, State(ds), , <a, b>, , {x:A| B(x)} , vartype(i;x), Top, f(x)?z, Knd, valtype(e), , A c B, left + right, P & Q, x:A. B(x), discrete state@i, (discrete state after e), isrcv(e), if b then t else f fi , x,y:A//B(x;y), True, f(a), T, , , A  B, EquivRel(T;x,y.E(x;y)), tt, qeq(r;s), x,y. t(x;y), sender(e), let x,y = A in B(x;y), source(l), Void, locl(a), P  Q, P  Q, Unit, case b of inl(x) => s(x) | inr(y) => t(y), x:A.B(x), rcv(l,tg), kind(e), Dec(P), discrete-weak-precond-send-p(es;T;A;l;tg;a;ds;P;f), weak-precond-send-p(es;T;A;l;tg;a;ds;P;f), x. t(x), state@i, (state when e), (state after e)+t, state after e

Lemmas

dds-state-after-elapsed, es-state-after-dstate-after, es-state-after-elapsed wf, es-state-when-dstate-when, es-state-when wf, es-state-subtype2, es-dstate wf, Knd sq, weak-precond-send-p wf, decl-state wf, fpf wf, Id wf, IdLnk wf, event system wf, es-dds wf, es-E wf, lsrc wf, es-causle wf, squash wf, decidable cand, decidable equal Kind, decidable es-le, Knd wf, es-kind wf, rcv wf, es-loc wf, not wf, true wf, false wf, es-isrcv-loc, es-le-loc, es-loc-pred, es-locl wf, es-le wf, es-sender wf, quotient wf, b-union wf, int nzero wf, bool wf, qeq wf2, btrue wf, rationals wf, assert wf, es-kind-rcv, es-dstate-after wf, es-dstate-subtype, Id sq